T:Type, eq:EqDecider(T), a, b:(T List).
l_disjoint(T;b;l_intersection(eq;a;b))  l_disjoint(T;a;b) 

latex

Definitions	x:A. B(x), (x  l), x:A  B(x), P & Q, Void, x:AB(x), P  Q, False, A, type List, EqDecider(T), Type, x.A(x), t  T, , l_intersection(eq;L1;L2), P  Q, P  Q, x. t(x), {T}, l_disjoint(T;l1;l2)
Lemmas	implies functionality wrt iff, all functionality wrt iff, not functionality wrt iff, and functionality wrt iff, member-intersection, deq wf, l intersection wf, l member wf, not wf